// experimenting with type-level computation in Scala:
// tuple that tracks the type for each of its components

// marker traits to use subtyping to simulate classification
trait Levels {
  // @inherit[private] trait Kind // class SomeTypeClassifier extends Kind ; class SomeValueClassifier extends SomeTypeClassifier ; NOT the case: SomeValueClassifier <: Kind
  // @inherit[private] trait OfKind[T <: Kind]
  /*@inherit[private]*/ trait Type // marker trait to distinguish types modelling kinds from their "inhabitants" (modelled as subtypes)
   // more precise name would be LowerThanKindLevel, as this marker gets inherited down the subclassing chain
  trait Value // similarly, but on value level -- kind of overkill since "abstract" kind of accomplishes the same thing (i.e., it says this type does NOT classify values)
   // more precise name would be LowerThanTypeLevel, as this marker gets inherited down the subclassing chain
}

trait Naturals extends Levels {
  
// the kind that classifies two types: TZero and TSucc  
  sealed trait KNatural { 
    type Pred <: TNatural

    type Match[Kind, Zero <: Kind, Succ[_ <: TNatural] <: Kind] <: Kind
    def matchWith[Kind, T <: Kind, U[_ <: TNatural] <: Kind]
        (zero: T, succ: TNatural => U[Pred]): Match[Kind, T, U]
  }
  
  abstract class TZero extends KNatural with Type {
    type Pred=Nothing
    
    type Match[Kind, Zero <: Kind, Succ[_ <: TNatural] <: Kind] = Zero
    def matchWith[Kind, T <: Kind, U[_ <: TNatural] <: Kind]
        (zero: T, succ: TNatural => U[Nothing]) = zero
  }
  
  // pred: _Pred --> pred must be _0, _1, ... as all other classes are abstract
  abstract class TSucc[_Pred <: TNatural](pred: _Pred) extends KNatural with
    Type {
    type Pred=_Pred
    
    type Match[Kind, Zero <: Kind, Succ[_ <: TNatural] <: Kind] = Succ[Pred]
    def matchWith[Kind, T <: Kind, U[_ <: TNatural] <: Kind]
        (zero: T, succ: TNatural => U[Pred]) = succ(pred)
  }
        
// T <: TNatural  means:  T is either TZero or TSucc  
// T <: Natural means T is a *singleton type* (_0.type, _1.type, ...)
  type Natural = TNatural with Value
  sealed trait TNatural extends KNatural with Type 
    object _0 extends TZero                   with Natural with Value
    object _1 extends TSucc[TZero](_0)        with Natural with Value
    object _2 extends TSucc[TSucc[TZero]](_1) with Natural with Value
    object _3 extends TSucc[TSucc[TSucc[TZero]]](_2) with Natural with Value
    
    // ..
}

trait Tuples extends Naturals {
  type TList[+Kind] = KList[Kind] with Type

  // the kind that classifies two types: TCons and TNil
  sealed abstract class KList[+Kind] { // experimenting with type-level computation in Scala:
// tuple that tracks the type for each of its components

// marker traits to use subtyping to simulate classification
trait Levels {
  // @inherit[private] trait Kind // class SomeTypeClassifier extends Kind ; class SomeValueClassifier extends SomeTypeClassifier ; NOT the case: SomeValueClassifier <: Kind
  // @inherit[private] trait OfKind[T <: Kind]
  /*@inherit[private]*/ trait Type // marker trait to distinguish types modelling kinds from their "inhabitants" (modelled as subtypes)
   // more precise name would be LowerThanKindLevel, as this marker gets inherited down the subclassing chain
  trait Value // similarly, but on value level -- kind of overkill since "abstract" kind of accomplishes the same thing (i.e., it says this type does NOT classify values)
   // more precise name would be LowerThanTypeLevel, as this marker gets inherited down the subclassing chain
}

trait Naturals extends Levels {
  
// the kind that classifies two types: TZero and TSucc  
  sealed trait KNatural { 
    type Pred <: TNatural

    type Match[Kind, Zero <: Kind, Succ[_ <: TNatural] <: Kind] <: Kind
    def matchWith[Kind, T <: Kind, U[_ <: TNatural] <: Kind]
        (zero: T, succ: TNatural => U[Pred]): Match[Kind, T, U]
  }
  
  abstract class TZero extends KNatural with Type {
    type Pred=Nothing
    
    type Match[Kind, Zero <: Kind, Succ[_ <: TNatural] <: Kind] = Zero
    def matchWith[Kind, T <: Kind, U[_ <: TNatural] <: Kind]
        (zero: T, succ: TNatural => U[Nothing]) = zero
  }
  
  // pred: _Pred --> pred must be _0, _1, ... as all other classes are abstract
  abstract class TSucc[_Pred <: TNatural](pred: _Pred) extends KNatural with
    Type {
    type Pred=_Pred
    
    type Match[Kind, Zero <: Kind, Succ[_ <: TNatural] <: Kind] = Succ[Pred]
    def matchWith[Kind, T <: Kind, U[_ <: TNatural] <: Kind]
        (zero: T, succ: TNatural => U[Pred]) = succ(pred)
  }
        
// T <: TNatural  means:  T is either TZero or TSucc  
// T <: Natural means T is a *singleton type* (_0.type, _1.type, ...)
  type Natural = TNatural with Value
  sealed trait TNatural extends KNatural with Type 
    object _0 extends TZero                   with Natural with Value
    object _1 extends TSucc[TZero](_0)        with Natural with Value
    object _2 extends TSucc[TSucc[TZero]](_1) with Natural with Value
    object _3 extends TSucc[TSucc[TSucc[TZero]]](_2) with Natural with Value
    
    // ..
}

trait Tuples extends Naturals {
  type TList[+Kind] = KList[Kind] with Type

  // the kind that classifies two types: TCons and TNil
  sealed abstract class KList[+Kind] { 
    // return the i'th type in this list of types
    type Get[i <: Natural] <: Kind
  }
  
  sealed class TCons[Head <: Kind, Tail <: TList[Kind], +Kind]
    extends KList[Kind] with Type {
    // not allowed to select abstract type on abstract type 
    // (allowing types like i#Match or Tail#Get probably makes typing undecidable, although it should be sound:
      // i#Match is sound because i is intended to be a singleton type
      // Tail#Get is sound because Tail is either TNil or TCons, both concrete classes
    type Get[i <: Natural] = Nothing // TODO: i#Match[Kind, Head, Tail#Get]
  }

  sealed class TNil extends KList[Nothing] with Type {
    type Get[i <: Natural] = Nothing // or Any, depending on taste
  }

  sealed abstract class Tuple {
    type Types <: TList[Any] 
    def ~:[T](x: T) = new ~:[T, this.type](x, this)
  
    // return the i'th component with its exact type 
    // (at this point this type is some unknown subtype of Any, 
    // but at valid call-sites for apply, everything can be checked statically)
    //TODO def apply(i: Natural): Types#Get[i.type]
  }
  
  case class ~:[Head, Tail <: Tuple](hd: Head, tail: Tail) extends Tuple with
    Value {
    type Types = TCons[Head, tail.Types, Any]

   //TODO def apply(i: Natural): Types#Get[i.type] = i.matchWith[Any, Head, tail.Types#Get](hd, pred => tail(pred))
   // : TCons[Head, tail.Types, Any]#Get[i.type]
   // : i.type#Match[Any, Head, tail.Types#Get]   // : i.type#Match[Any, Head, tail.Types#Get]
  }
  
  case class <> extends Tuple with Value {
    type Types = TNil
    
    def apply(i: Natural) = error("Indexing empty tuple")        
  }
}

object main extends Tuples {
  val x: Int ~: Int ~: String ~: <> = 1 ~: 2 ~: "a" ~: <>
  //TODO x(_0) : Int  
  //TODO x(_1) : Int  
  //TODO x(_2) : String

    // return the i'th type in this list of types
    type Get[i <: Natural] <: Kind
  }
  
  sealed class TCons[Head <: Kind, Tail <: TList[Kind], +Kind]
    extends KList[Kind] with Type {
    // not allowed to select abstract type on abstract type 
    // (allowing types like i#Match or Tail#Get probably makes typing undecidable, although it should be sound:
      // i#Match is sound because i is intended to be a singleton type
      // Tail#Get is sound because Tail is either TNil or TCons, both concrete classes
    type Get[i <: Natural] = Nothing // TODO: i#Match[Kind, Head, Tail#Get]
  }

  sealed class TNil extends KList[Nothing] with Type {
    type Get[i <: Natural] = Nothing // or Any, depending on taste
  }

  sealed abstract class Tuple {
    type Types <: TList[Any] 
    def ~:[T](x: T) = new ~:[T, this.type](x, this)
  
    // return the i'th component with its exact type 
    // (at this point this type is some unknown subtype of Any, 
    // but at valid call-sites for apply, everything can be checked statically)
    //TODO def apply(i: Natural): Types#Get[i.type]
  }
  
  case class ~:[Head, Tail <: Tuple](hd: Head, tail: Tail) extends Tuple with
    Value {
    type Types = TCons[Head, tail.Types, Any]

   //TODO def apply(i: Natural): Types#Get[i.type] = i.matchWith[Any, Head, tail.Types#Get](hd, pred => tail(pred))
   // : TCons[Head, tail.Types, Any]#Get[i.type]
   // : i.type#Match[Any, Head, tail.Types#Get]   // : i.type#Match[Any, Head, tail.Types#Get]
  }
  
  case class <> extends Tuple with Value {
    type Types = TNil
    
    def apply(i: Natural) = error("Indexing empty tuple")        
  }
}

object main extends Tuples {
  val x: Int ~: Int ~: String ~: <> = 1 ~: 2 ~: "a" ~: <>
  //TODO x(_0) : Int  
  //TODO x(_1) : Int  
  //TODO x(_2) : String
}